predicate app (f, x) = f (x)
lemma apply_ok : forall (x : int). app (fun x -> (x = x), x)
